Формальные методы

Пример формальной спецификации с использованием Z-нотации

В информатике и инженерии программного обеспечения формальными методами (англ. formal methods) называется группа техник, основанных на математическом аппарате для спецификации, разработки и верификации программного и аппаратного обеспечения. Использование формальных методов для проектирования программного и аппаратного обеспечения обусловлено ожиданиями того, что, как и в других инженерных областях, использование математического анализа может существенно поднять надёжность систем. При этом формальные методы довольно сложны, требуют специальной подготовки, временных и ресурсных вложений, и при этом нередко основываются на не всегда достижимых в реальных условиях предположениях. Это приводит к тому, что формальные методы чаще всего находят применение в проектировании высокоточных систем, где важность безопасности оправдывает любые средства.

Формальные методы занимаются приложением довольно широкого класса фундаментальных техник теоретической информатики: разные исчисления логики, формальных языков, теории автоматов, формальной семантики, систем типов и алгебраических типов данных.

Разновидности формальных методов

Можно выделить три уровня применения формальных методов:

Нулевой уровень

Разрабатывается формальная спецификация, затем программный код пишется, глядя на неё. В этом случае пропасть между формальной и неформальной частью остаётся бездоказательной, но решение может быть эффективным с точки зрения его стоимости.

Первый уровень

Программный код выводится из формальной спецификации автоматически, используются механизмы верификации, доказываются наиболее критичные свойства системы. Этот путь зачастую выбирается для высокоточных систем.

Второй уровень

Автоматические доказатели теорем используются для выведения полностью формализованных доказательств, проверяемых автоматически. Подход требует объёмных вложений и исследований, но оправдывает себя в самых критичных частях сложных систем, где ошибки непозволительны (например, в проектировании интегральных схем).

Подходы к формальным методам также можно классифицировать аналогично формальной семантике языков программирования:

Денотационная семантика (англ. denotational semantics)

Значение системы выражается через частично упорядоченные множества, а методы полагаются на хорошо разработанную теорию вокруг них. Ограничение метода — в том, что не каждая система может быть интуитивно или естественно рассмотрена как функция.

Операционная семантика (англ. operational semantics)

Значение системы обозначается последовательностью действий в рамках более простой вычислительной модели (например, лямбда-исчисления или сетей Петри). Методы славятся своей простотой, если не акцентировать внимание на том, что они полагаются на семантику «более простой» системы, которую тоже надо через что-то определять.

Аксиоматическая семантика (англ. axiomatic semantics)

Смысл системы определяется в терминах предусловий и постусловий, что позволяет связать теорию с классической логикой, но не даёт представления о том, что конкретно происходит внутри системы (как достигаются постусловия на основе предусловий).

Кроме того, нередко резко положительных результатов можно достичь, пожертвовав глобальной применимостью и сверхформализацией — такие случаи называют «облегчёнными» (lightweight) формальными методами. Их можно разделить на два типа: с усиленной и с ослабленной автоматизацией. Пример усиленной автоматизации — анализатор спецификаций Alloy Analyzer, который для того, чтобы свести задачу поиска модели к решаемой, сужая область поиска (в результате Аллой работает полностью автоматизированно, в отличие от интерактивных доказателей, но имеет шанс не найти некоторые проблемы). Пример ослабленной — сходимость грамматик, в которой неразрешимость задачи эквивалентности двух формальных языков обходится тем, что преобразования совершает сам человек, а выводы делаются уже по свойствам использованных им операторов.

Использование формальных методов

Формальные методы применяются на разных этапах разработки программного обеспечения:

Спецификация

С помощью формальных методов можно описать будущую систему с любым уровнем детализации. Такое формальное описание может напрямую или опосредовано с пользой использоваться на более поздних этапах. При этом работа по доказательству ряда требуемых функциональных свойств может начинаться сразу и идти параллельно с написанием или генерацией кода. Существует целый ряд языков и исчислений для формальных спецификаций, но ни один не может претендовать на звание универсального, как Форма Бэкуса — Наура для спецификации синтаксиса.

Разработка

Если формальная спецификация использует операциональную семантику, наблюдаемое поведение конкретной системы можно сравнивать с ожидаемым, потому что такая семантика может быть выполнимой, а может даже использоваться для автоматического генерирования кода. Если используется аксиоматическая семантика, то предусловия и постусловия могут напрямую отобразиться в утверждения в выполнимом коде.

Верификация

Когда формальная спецификация подготовлена, её можно использовать для доказательства требуемых свойств. Верификация бывает дедуктивной и модельной: дедуктивная использует автоматическое доказательство теорем или специфические алгебры, а модельная основывает свои выводы не на самой системе, а на построенной по ней модели. При этом модель совершенно не обязательно строить вручную, если применимы оказываются техники вроде программного сечения.

Критика формальных методов

Доказательства вручную требуют серьёзных вложений ресурсов и не дают никакой выгоды, кроме подтверждения правильности. В результате формальные методы используются или в тех областях, где доказательства можно получить автоматически программным путём, или в тех, где цена ошибки слишком высока (например, при создании космических аппаратов или магнитно-резонансных томографов).

Абстракции, нотации и языки формальных методов

• Абстрактная интерпретация
• Абстрактный автомат (ASM)
  • Конечный автомат (FSM)
  • Машина Тьюринга
  • Модель Крипке
• Автомат Бюхи
• Alloy Analyzer
• Анализ программного кода и построенных по нему графов:
  • Анализ потока данных (DFA)
  • Анализ потока управления (CFA)
  • Динамический анализ кода
  • Статический анализ кода
• B-метод
• Венский метод разработки (VDM, VDM-SL, VDM+)
• Единый язык алгебраических спецификаций (CASL) и программа Hets
• Исчисления процессов:
  • Алгебра общающихся систем (ACP)
  • Взаимодействующие последовательные процессы Хоара (CSP)
  • Исчисление общающихся систем
  • пи-исчисление
  • LOTOS, E-LOTOS
• Lustre
• Лямбда-исчисление, включая типизированное
• Модель акторов
• Переписывание (TRS)
• Промела и верификатор моделей SPIN
• Ребека
• Сети Петри
• Создание и анализ распределённых процессов (CADP)
• Темпоральная логика (особенно TLA+ и PlusCal)
• Универсальный язык систем (USL)
• Эстерел
• Язык спецификации ANSI/ISO C (ACSL) и верификатор Frama-C
• Specification and Description Language (SDL)
• Z-нотация

Литература

• Lathouwers, Sophie; Zaytsev, Vadim (2022). "Modelling Program Verification Tools for Software Engineers". Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems. MODELS '22. Montreal, Quebec, Canada: Association for Computing Machinery. pp. 98—108. doi:10.1145/3550355.3552426. ISBN 9781450394666.

Ссылки

• Formal Methods Europe (FME)
• FM — Международный симпозиум по формальным методам, престижная конференция
• ICFEM — Международная конференция по формальным инженерным методам, конференция IEEE ненамного ниже уровнем
• IFM — Международная конференция по интегрированным формальным методам, конференция одного уровня с ICFEM
• Sophie Lathouwers, Vadim Zaytsev. ProVerB: Program Verification Book (англ.). (один из вариантов классификации и большой список средств формальной верификации)